<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- NewPage -->
<html lang="en">
<head>
<title>ProofWorksheetParser</title>
<link rel="stylesheet" type="text/css" href="../../stylesheet.css" title="Style">
</head>
<body>
<script type="text/javascript"><!--
    if (location.href.indexOf('is-external=true') == -1) {
        parent.document.title="ProofWorksheetParser";
    }
//-->
</script>
<noscript>
<div>JavaScript is disabled on your browser.</div>
</noscript>
<!-- ========= START OF TOP NAVBAR ======= -->
<div class="topNav"><a name="navbar_top">
<!--   -->
</a><a href="#skip-navbar_top" title="Skip navigation links"></a><a name="navbar_top_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/pa/ProofWorksheet.html" title="class in mmj.pa"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/pa/ProofWorkStmt.html" title="class in mmj.pa"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/pa/ProofWorksheetParser.html" target="_top">Frames</a></li>
<li><a href="ProofWorksheetParser.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_top">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_top");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_top">
<!--   -->
</a></div>
<!-- ========= END OF TOP NAVBAR ========= -->
<!-- ======== START OF CLASS DATA ======== -->
<div class="header">
<div class="subTitle">mmj.pa</div>
<h2 title="Class ProofWorksheetParser" class="title">Class ProofWorksheetParser</h2>
</div>
<div class="contentContainer">
<ul class="inheritance">
<li>java.lang.Object</li>
<li>
<ul class="inheritance">
<li>mmj.pa.ProofWorksheetParser</li>
</ul>
</li>
</ul>
<div class="description">
<ul class="blockList">
<li class="blockList">
<hr>
<br>
<pre>public class <span class="strong">ProofWorksheetParser</span>
extends java.lang.Object</pre>
<div class="block">ProofWorksheetParser handles the details of iteration through 1 or more
 ProofWorksheets input via String, File or Reader.
 <p>
 The big shortcoming that it has right now, which may not be big depending on
 your plans, is that an input ProofWorksheet with structural errors or other
 severe errors, throws an exception and leaves the input stream stuck in the
 middle of the worksheet tokens. An enhancement might be to add a routine to
 chunk through the input stream and bypass tokens until a proof worksheet
 "Footer" is found, and then grab the *next* token, which could be used to
 initiate and parse the following ProofWorksheet. However, at this time,
 batches of ProofWorksheets are used only in testing, so no energy has been
 expended in bypassing an errored ProofWorksheet's remaining tokens.</div>
</li>
</ul>
</div>
<div class="summary">
<ul class="blockList">
<li class="blockList">
<!-- ======== CONSTRUCTOR SUMMARY ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_summary">
<!--   -->
</a>
<h3>Constructor Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Constructor Summary table, listing constructors, and an explanation">
<caption><span>Constructors</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colOne" scope="col">Constructor and Description</th>
</tr>
<tr class="altColor">
<td class="colOne"><code><strong><a href="../../mmj/pa/ProofWorksheetParser.html#ProofWorksheetParser(java.io.File, java.lang.String, mmj.pa.ProofAsstPreferences, mmj.lang.LogicalSystem, mmj.verify.Grammar, mmj.lang.Messages)">ProofWorksheetParser</a></strong>(java.io.File&nbsp;proofFile,
                    java.lang.String&nbsp;proofTextSource,
                    <a href="../../mmj/pa/ProofAsstPreferences.html" title="class in mmj.pa">ProofAsstPreferences</a>&nbsp;proofAsstPreferences,
                    <a href="../../mmj/lang/LogicalSystem.html" title="class in mmj.lang">LogicalSystem</a>&nbsp;logicalSystem,
                    <a href="../../mmj/verify/Grammar.html" title="class in mmj.verify">Grammar</a>&nbsp;grammar,
                    <a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages)</code>
<div class="block">Constructor.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colOne"><code><strong><a href="../../mmj/pa/ProofWorksheetParser.html#ProofWorksheetParser(java.io.Reader, java.lang.String, mmj.pa.ProofAsstPreferences, mmj.lang.LogicalSystem, mmj.verify.Grammar, mmj.lang.Messages)">ProofWorksheetParser</a></strong>(java.io.Reader&nbsp;proofTextReader,
                    java.lang.String&nbsp;proofTextSource,
                    <a href="../../mmj/pa/ProofAsstPreferences.html" title="class in mmj.pa">ProofAsstPreferences</a>&nbsp;proofAsstPreferences,
                    <a href="../../mmj/lang/LogicalSystem.html" title="class in mmj.lang">LogicalSystem</a>&nbsp;logicalSystem,
                    <a href="../../mmj/verify/Grammar.html" title="class in mmj.verify">Grammar</a>&nbsp;grammar,
                    <a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages)</code>
<div class="block">Constructor.</div>
</td>
</tr>
<tr class="altColor">
<td class="colOne"><code><strong><a href="../../mmj/pa/ProofWorksheetParser.html#ProofWorksheetParser(java.lang.String, java.lang.String, mmj.pa.ProofAsstPreferences, mmj.lang.LogicalSystem, mmj.verify.Grammar, mmj.lang.Messages)">ProofWorksheetParser</a></strong>(java.lang.String&nbsp;proofText,
                    java.lang.String&nbsp;proofTextSource,
                    <a href="../../mmj/pa/ProofAsstPreferences.html" title="class in mmj.pa">ProofAsstPreferences</a>&nbsp;proofAsstPreferences,
                    <a href="../../mmj/lang/LogicalSystem.html" title="class in mmj.lang">LogicalSystem</a>&nbsp;logicalSystem,
                    <a href="../../mmj/verify/Grammar.html" title="class in mmj.verify">Grammar</a>&nbsp;grammar,
                    <a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages)</code>
<div class="block">Constructor.</div>
</td>
</tr>
</table>
</li>
</ul>
<!-- ========== METHOD SUMMARY =========== -->
<ul class="blockList">
<li class="blockList"><a name="method_summary">
<!--   -->
</a>
<h3>Method Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Method Summary table, listing methods, and an explanation">
<caption><span>Methods</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colFirst" scope="col">Modifier and Type</th>
<th class="colLast" scope="col">Method and Description</th>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofWorksheetParser.html#closeReader()">closeReader</a></strong>()</code>
<div class="block">Closes the ProofWorksheet token reader.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>boolean</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofWorksheetParser.html#hasNext()">hasNext</a></strong>()</code>
<div class="block">Checks to see if another ProofWorksheet is available.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code><a href="../../mmj/pa/ProofWorksheet.html" title="class in mmj.pa">ProofWorksheet</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofWorksheetParser.html#next()">next</a></strong>()</code>
<div class="block">Returns the next ProofWorksheet from the input source for situations when
 input cursor position not available.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code><a href="../../mmj/pa/ProofWorksheet.html" title="class in mmj.pa">ProofWorksheet</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofWorksheetParser.html#next(int, mmj.pa.StepRequest)">next</a></strong>(int&nbsp;inputCursorPos,
    <a href="../../mmj/pa/StepRequest.html" title="class in mmj.pa">StepRequest</a>&nbsp;stepRequest)</code>
<div class="block">Returns the next ProofWorksheet from the input source.</div>
</td>
</tr>
</table>
<ul class="blockList">
<li class="blockList"><a name="methods_inherited_from_class_java.lang.Object">
<!--   -->
</a>
<h3>Methods inherited from class&nbsp;java.lang.Object</h3>
<code>clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait</code></li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
<div class="details">
<ul class="blockList">
<li class="blockList">
<!-- ========= CONSTRUCTOR DETAIL ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_detail">
<!--   -->
</a>
<h3>Constructor Detail</h3>
<a name="ProofWorksheetParser(java.io.Reader, java.lang.String, mmj.pa.ProofAsstPreferences, mmj.lang.LogicalSystem, mmj.verify.Grammar, mmj.lang.Messages)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>ProofWorksheetParser</h4>
<pre>public&nbsp;ProofWorksheetParser(java.io.Reader&nbsp;proofTextReader,
                    java.lang.String&nbsp;proofTextSource,
                    <a href="../../mmj/pa/ProofAsstPreferences.html" title="class in mmj.pa">ProofAsstPreferences</a>&nbsp;proofAsstPreferences,
                    <a href="../../mmj/lang/LogicalSystem.html" title="class in mmj.lang">LogicalSystem</a>&nbsp;logicalSystem,
                    <a href="../../mmj/verify/Grammar.html" title="class in mmj.verify">Grammar</a>&nbsp;grammar,
                    <a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages)
                     throws java.io.IOException,
                            <a href="../../mmj/mmio/MMIOError.html" title="class in mmj.mmio">MMIOError</a></pre>
<div class="block">Constructor.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>proofTextReader</code> - Reader of ProofWorksheet tokens</dd><dd><code>proofTextSource</code> - Comment for debugging/testing</dd><dd><code>proofAsstPreferences</code> - variable settings</dd><dd><code>logicalSystem</code> - the loaded Metamath data</dd><dd><code>grammar</code> - the mmj.verify.Grammar object</dd><dd><code>messages</code> - the mmj.lang.Messages object used to store error and
            informational messages.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code>java.io.IOException</code> - if an error occurred</dd>
<dd><code><a href="../../mmj/mmio/MMIOError.html" title="class in mmj.mmio">MMIOError</a></code> - if an error occurred</dd></dl>
</li>
</ul>
<a name="ProofWorksheetParser(java.lang.String, java.lang.String, mmj.pa.ProofAsstPreferences, mmj.lang.LogicalSystem, mmj.verify.Grammar, mmj.lang.Messages)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>ProofWorksheetParser</h4>
<pre>public&nbsp;ProofWorksheetParser(java.lang.String&nbsp;proofText,
                    java.lang.String&nbsp;proofTextSource,
                    <a href="../../mmj/pa/ProofAsstPreferences.html" title="class in mmj.pa">ProofAsstPreferences</a>&nbsp;proofAsstPreferences,
                    <a href="../../mmj/lang/LogicalSystem.html" title="class in mmj.lang">LogicalSystem</a>&nbsp;logicalSystem,
                    <a href="../../mmj/verify/Grammar.html" title="class in mmj.verify">Grammar</a>&nbsp;grammar,
                    <a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages)
                     throws java.io.IOException,
                            <a href="../../mmj/mmio/MMIOError.html" title="class in mmj.mmio">MMIOError</a></pre>
<div class="block">Constructor.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>proofText</code> - String containing ProofWorksheet tokens</dd><dd><code>proofTextSource</code> - Comment for debugging/testing</dd><dd><code>proofAsstPreferences</code> - variable settings</dd><dd><code>logicalSystem</code> - the loaded Metamath data</dd><dd><code>grammar</code> - the mmj.verify.Grammar object</dd><dd><code>messages</code> - the mmj.lang.Messages object used to store error and
            informational messages.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code>java.io.IOException</code> - if an error occurred</dd>
<dd><code><a href="../../mmj/mmio/MMIOError.html" title="class in mmj.mmio">MMIOError</a></code> - if an error occurred</dd></dl>
</li>
</ul>
<a name="ProofWorksheetParser(java.io.File, java.lang.String, mmj.pa.ProofAsstPreferences, mmj.lang.LogicalSystem, mmj.verify.Grammar, mmj.lang.Messages)">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>ProofWorksheetParser</h4>
<pre>public&nbsp;ProofWorksheetParser(java.io.File&nbsp;proofFile,
                    java.lang.String&nbsp;proofTextSource,
                    <a href="../../mmj/pa/ProofAsstPreferences.html" title="class in mmj.pa">ProofAsstPreferences</a>&nbsp;proofAsstPreferences,
                    <a href="../../mmj/lang/LogicalSystem.html" title="class in mmj.lang">LogicalSystem</a>&nbsp;logicalSystem,
                    <a href="../../mmj/verify/Grammar.html" title="class in mmj.verify">Grammar</a>&nbsp;grammar,
                    <a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages)
                     throws java.io.IOException,
                            <a href="../../mmj/mmio/MMIOError.html" title="class in mmj.mmio">MMIOError</a></pre>
<div class="block">Constructor.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>proofFile</code> - File object specifying ProofWorksheet token file for
            input.</dd><dd><code>proofTextSource</code> - Comment for debugging/testing</dd><dd><code>proofAsstPreferences</code> - variable settings</dd><dd><code>logicalSystem</code> - the loaded Metamath data</dd><dd><code>grammar</code> - the mmj.verify.Grammar object</dd><dd><code>messages</code> - the mmj.lang.Messages object used to store error and
            informational messages.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code>java.io.IOException</code> - if an error occurred</dd>
<dd><code><a href="../../mmj/mmio/MMIOError.html" title="class in mmj.mmio">MMIOError</a></code> - if an error occurred</dd></dl>
</li>
</ul>
</li>
</ul>
<!-- ============ METHOD DETAIL ========== -->
<ul class="blockList">
<li class="blockList"><a name="method_detail">
<!--   -->
</a>
<h3>Method Detail</h3>
<a name="closeReader()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>closeReader</h4>
<pre>public&nbsp;void&nbsp;closeReader()</pre>
<div class="block">Closes the ProofWorksheet token reader.
 <p>
 Use this when finished, it doesn't get called automatically!</div>
</li>
</ul>
<a name="hasNext()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>hasNext</h4>
<pre>public&nbsp;boolean&nbsp;hasNext()</pre>
<div class="block">Checks to see if another ProofWorksheet is available.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>true if at least one more ProofWorksheet token exists to be
         processed.</dd></dl>
</li>
</ul>
<a name="next()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>next</h4>
<pre>public&nbsp;<a href="../../mmj/pa/ProofWorksheet.html" title="class in mmj.pa">ProofWorksheet</a>&nbsp;next()
                    throws java.io.IOException,
                           <a href="../../mmj/mmio/MMIOError.html" title="class in mmj.mmio">MMIOError</a>,
                           <a href="../../mmj/pa/ProofAsstException.html" title="class in mmj.pa">ProofAsstException</a></pre>
<div class="block">Returns the next ProofWorksheet from the input source for situations when
 input cursor position not available.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>ProofWorksheet or throws an exception!</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code>java.io.IOException</code> - if an error occurred</dd>
<dd><code><a href="../../mmj/mmio/MMIOError.html" title="class in mmj.mmio">MMIOError</a></code> - if an error occurred</dd>
<dd><code><a href="../../mmj/pa/ProofAsstException.html" title="class in mmj.pa">ProofAsstException</a></code> - if an error occurred</dd></dl>
</li>
</ul>
<a name="next(int, mmj.pa.StepRequest)">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>next</h4>
<pre>public&nbsp;<a href="../../mmj/pa/ProofWorksheet.html" title="class in mmj.pa">ProofWorksheet</a>&nbsp;next(int&nbsp;inputCursorPos,
                  <a href="../../mmj/pa/StepRequest.html" title="class in mmj.pa">StepRequest</a>&nbsp;stepRequest)
                    throws java.io.IOException,
                           <a href="../../mmj/mmio/MMIOError.html" title="class in mmj.mmio">MMIOError</a>,
                           <a href="../../mmj/pa/ProofAsstException.html" title="class in mmj.pa">ProofAsstException</a></pre>
<div class="block">Returns the next ProofWorksheet from the input source.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>inputCursorPos</code> - offset plus one of Caret in Proof TextArea;</dd><dd><code>stepRequest</code> - may be null, or StepSelector Search or Choice request
            and will be loaded into the ProofWorksheet.</dd>
<dt><span class="strong">Returns:</span></dt><dd>ProofWorksheet or throws an exception!</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code>java.io.IOException</code> - if an error occurred</dd>
<dd><code><a href="../../mmj/mmio/MMIOError.html" title="class in mmj.mmio">MMIOError</a></code> - if an error occurred</dd>
<dd><code><a href="../../mmj/pa/ProofAsstException.html" title="class in mmj.pa">ProofAsstException</a></code> - if an error occurred</dd></dl>
</li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
</div>
<!-- ========= END OF CLASS DATA ========= -->
<!-- ======= START OF BOTTOM NAVBAR ====== -->
<div class="bottomNav"><a name="navbar_bottom">
<!--   -->
</a><a href="#skip-navbar_bottom" title="Skip navigation links"></a><a name="navbar_bottom_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/pa/ProofWorksheet.html" title="class in mmj.pa"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/pa/ProofWorkStmt.html" title="class in mmj.pa"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/pa/ProofWorksheetParser.html" target="_top">Frames</a></li>
<li><a href="ProofWorksheetParser.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_bottom">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_bottom");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_bottom">
<!--   -->
</a></div>
<!-- ======== END OF BOTTOM NAVBAR ======= -->
</body>
</html>
